# Addheader.py Use with care, it's hacky. [[todo]] Think about which other trivial tools could belong in tools/.